/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Class for constructing inductive datatypes that correspond to
 * grammars that encode syntactic restrictions for SyGuS.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_NEW_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_NEW_H

#include <map>
#include <vector>

#include "expr/node.h"
#include "expr/sygus_grammar.h"
#include "smt/env.h"

namespace cvc5::internal {
namespace theory {
namespace quantifiers {

/**
 * Utility for constructing datatypes that correspond to syntactic restrictions.
 */
class SygusGrammarCons
{
 public:
  /**
   * Make the type corresponding to the default sygus grammar type returning
   * range with bound variables bvl.
   *
   * @param env The environment, which impacts grammar construction
   * @param range The type of terms generated by the start symbol of the
   * grammar.
   * @param bvl The input variable list for the grammar (if it exists). If
   * provided, each variable in this list is added as a terminal rule.
   */
  static TypeNode mkDefaultSygusType(const Env& env,
                                     const TypeNode& range,
                                     const Node& bvl);
  /**
   * Make the type corresponding to the default sygus grammar type returning
   * range with bound variables bvl, with a custom set of initial terminal
   * rules.
   *
   * @param env The environment, which impacts grammar construction
   * @param range The type of terms generated by the start symbol of the
   * grammar.
   * @param bvl The input variable list for the grammar (if it exists).
   * @param trules The provided set of terminal rules.
   */
  static TypeNode mkDefaultSygusType(const Env& env,
                                     const TypeNode& range,
                                     const Node& bvl,
                                     const std::vector<Node>& trules);

  /**
   * Make the default sygus grammar type returning range with bound variables
   * bvl.
   *
   * @param env The environment, which impacts grammar construction
   * @param range The type of terms generated by the start symbol of the
   * grammar.
   * @param bvl The input variable list for the grammar (if it exists). If
   * provided, each variable in this list is added as a terminal rule.
   */
  static SygusGrammar mkDefaultGrammar(const Env& env,
                                       const TypeNode& range,
                                       const Node& bvl);

  /**
   * Make the default sygus grammar type returning range with bound variables
   * bvl, with a custom set of initial terminal rules.
   *
   * @param env The environment, which impacts grammar construction
   * @param range The type of terms generated by the start symbol of the
   * grammar.
   * @param bvl The input variable list for the grammar (if it exists).
   * @param trules The provided set of terminal rules.
   */
  static SygusGrammar mkDefaultGrammar(const Env& env,
                                       const TypeNode& range,
                                       const Node& bvl,
                                       const std::vector<Node>& trules);

  /**
   * Make the builtin constants for type "type" that should be included in a
   * sygus grammar, add them to vector ops.
   * 
   * @param type The type to add constants for
   * @param op The vector to add the constants to
   */
  static void mkSygusConstantsForType(const TypeNode& type,
                                      std::vector<Node>& ops);

 private:
  /**
   * Make the default sygus grammar type returning range with bound variables
   * bvl, with a custom set of initial terminal rules.
   *
   * @param env The environment, which impacts grammar construction
   * @param range The type of terms generated by the start symbol of the
   * grammar.
   * @param bvl The input variable list for the grammar (if it exists).
   * @param trules The provided set of terminal rules.
   */
  static SygusGrammar mkEmptyGrammar(const Env& env,
                                     const TypeNode& range,
                                     const Node& bvl,
                                     const std::vector<Node>& trules);
  /**
   * This adds to types the types we should consider in the sygus grammar
   * for the type range. This is the component types of range plus other
   * auxiliary types for defining operators in its theory.
   */
  static void collectTypes(const TypeNode& range,
                           std::unordered_set<TypeNode>& types);
  /**
   * Adds the default rules for non-terminal ntSym to g, where ntSym is a
   * non-terminal of g. This may additionally add rules to other non-terminals
   * of g, e.g. based on theory symbols that have types different from ntSym,
   * e.g. array select.
   *
   * This is done in stages (based on the argument stage). In the first
   * stage, we add all basic rules. In the second stage, we consider rules
   * that depend on rules added in previous stages, e.g. monomials for operators
   * that are constructed from symbols belonging to non-arithmetic theories.
   */
  static void addDefaultRulesTo(
      const Env& env,
      SygusGrammar& g,
      const Node& ntSym,
      const std::map<TypeNode, std::vector<Node>>& typeToNtSym,
      size_t stage);
  /**
   * Adds the default predicate rules for non-terminal ntSymBool to g, where
   * ntSymBool is a Boolean non-terminal of g.
   */
  static void addDefaultPredicateRulesTo(
      const Env& env,
      SygusGrammar& g,
      const Node& ntSym,
      const Node& ntSymBool,
      const std::map<TypeNode, std::vector<Node>>& typeToNtSym);
  /**
   * Computes a mapping from types to the non-terminals in g with that
   * type.
   */
  static std::map<TypeNode, std::vector<Node>> getTypeToNtSymMap(
      const SygusGrammar& g);
  /**
   * Adds a rule for a term whose operator is kind k and has argument types
   * given by args. The canonical non-terminals for each type is given by
   * typeToNtSym.
   *
   * This method returns true if a rule was added to g. This may fail if there
   * is no non-terminal for a type in args or for the return type of the
   * constructed term.
   */
  static bool addRuleTo(
      SygusGrammar& g,
      const std::map<TypeNode, std::vector<Node>>& typeToNtSym,
      Kind k,
      const std::vector<TypeNode>& args);
  /**
   * Similar to the above method.
   *
   * Adds a rule for a term whose operator is kind k and operator op and has
   * argument types given by args. The non-terminals for each type is
   * given by typeToNtSym.
   *
   * This method returns true if a rule was added to g. This may fail if there
   * is no non-terminal for a type in args or for the return type of the
   * constructed term.
   */
  static bool addRuleTo(
      SygusGrammar& g,
      const std::map<TypeNode, std::vector<Node>>& typeToNtSym,
      Kind k,
      const Node& op,
      const std::vector<TypeNode>& args);
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5::internal

#endif
